﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.IO;
using System.Diagnostics;
using System.Threading;

namespace OpSatPlan.SatSolvers
{
    public abstract class SatSolver
    {
        private string[] mOutput;

        public abstract bool?[] Model
        {
            get;
        }

        public abstract string Name
        {
            get;
        }

        protected abstract string ExecutableName
        {
            get;
        }

        protected abstract string Arguments(string cnfFileName);

        public bool Solve(int timeLeft, string cnfFileName)
        {
            Process process;
            Stopwatch stopwatch;
            Thread processThread;

            this.mOutput = null;

            stopwatch = new Stopwatch();

            processThread = new Thread(this.ProcessOutput);
            
            process = new Process();
            process.StartInfo.UseShellExecute = false;
            process.StartInfo.RedirectStandardOutput = true;
            process.StartInfo.FileName = this.ExecutableName;
            process.StartInfo.Arguments = this.Arguments(cnfFileName);

            // start timer, process and output processing thread
            stopwatch.Start();
            process.Start();
            processThread.Start(process);
            
            // block process for total time to read output
            if (!processThread.Join(timeLeft))
                process.Kill();

            // stop the timer
            stopwatch.Stop();

            Assertion.Assert<TimeLimitException>(stopwatch.ElapsedMilliseconds < timeLeft, "Time limit exceeded");
            return this.IsSat(this.mOutput);
        }

        public abstract void Reset();

        protected abstract bool IsSat(string[] lines);

        /// <summary>
        /// proc is type Process. While process is executing, read from standard output until
        /// null is returned.
        /// </summary>
        /// <param name="proc"></param>
        private void ProcessOutput(object proc)
        {
            string line;
            List<string> lines = new List<string>();
            Process process = (Process)proc;
            while ((line = process.StandardOutput.ReadLine()) != null)
            {
                lines.Add(line);
            }
            this.mOutput = lines.ToArray();
        }
    }
}
